#ifndef IC3_ADT_H
#define IC3_ADT_H

#include <vec.h>
#include <tr1/unordered_map>
#include "minisat-2.2/Solver.h"  
#include <algorithm>

typedef uint64_t * State;
typedef Minisat::vec< Minisat::Lit > Clause; 

/**
@brief recording the bug tracing state 

foreach <state,level>
   there is a bug-trace from state ( really trace )
   such state is inductively invariant to level-1 

   so it need to check is any path exist to state, 
   if one , such witness is inductive invariant to level - 2 
*/
class States
{
   struct StEq
   {
      bool operator()( const State a , const State b )const
      {
         for( unsigned i = 0 ; i < _wstates; ++i ) 
            if(a[i]!=b[i])return false; 
         return true;
      }
      StEq( unsigned st):_wstates(st){}
      unsigned _wstates;
   };
   struct StKey
   {
      size_t operator()( const State a )const
      {
         size_t s = 0;
         for( unsigned i = 0 ; i < _wstates ; ++ i )
            s ^= a[i];
         return s;
      }
      StKey( unsigned st):_wstates(st){}
      unsigned _wstates;
   };
   struct Cmp // less Comparator using in Heap
   {
      bool operator()( const std::pair<unsigned,State> & a , const std::pair<unsigned,State> & b)const{ 
         return b.first < a.first;}
   };

   typedef std::tr1::unordered_map< State , unsigned , StKey , StEq > Hash;

   Hash                              _hash;
   vec< std::pair<unsigned,State> >  _heap;
   Cmp                               _cmp;
   unsigned                          _wstates;

   public:

   States( unsigned n ): _hash( 10 , StKey(n) , StEq(n) ),_wstates(n){ };
   bool is0( State s ){ for( unsigned i = 0 ; i < _wstates ; ++ i )if( s[i]!= 0UL)return false;return true;}
   bool add( State s , unsigned l )
   {
      assert( is0(s) == false );
      Hash::iterator iter = _hash.find( s );
      if( iter != _hash.end() )
      {
         if( l >= iter->second ) return false;
         iter->second = l;

         _heap.push( std::make_pair( l , s ) );
         std::push_heap( _heap.data , _heap.data + _heap.sz , _cmp );
         return false;
      }else
      {
         _hash.insert( std::make_pair( s , l ) );

         _heap.push( std::make_pair( l , s ) );
         std::push_heap( _heap.data , _heap.data + _heap.sz  , _cmp);
         return true;
      }
   }
   /// pop and re push 
   void modify( unsigned l )
   {
      _hash[ state() ] = l;
      _heap[0].first = l;
      pop_heap( _heap.data , _heap.data + _heap.sz  , _cmp);
      push_heap(_heap.data , _heap.data + _heap.sz  , _cmp);
   }
   void extract()
   {
      if( _heap.size() == 1 )return; // accerleration 
      while( _heap[0].first != _hash[ _heap[0].second ] )
      {
         pop_heap( _heap.data , _heap.data + _heap.sz , _cmp );
         _heap.sz -= 1;
      }
   }
   inline State state(){ return _heap[0].second ;} 
   inline unsigned level(){return _heap[0].first;}

};


/**
@brief Class to keap the clause
The keaper here is implemented by tr1::hash , could be improve by google hash ( need additional keys , insertion only)
*/
class ClauseKeaper
{
   protected:

   typedef struct
   {
      const Clause * _ptr;
      unsigned       _lvl;
   }clause_t;

   struct CKHashFun
   {
      size_t operator()( const Clause * in ) const 
      { 
         const Minisat::Lit * c = in->data;
         unsigned sz = in->size();

         size_t k=sz;
         for( unsigned i = 0 ; i < sz ; ++ i ) k ^= c[i].x;
         return k;
      }
   };

   struct CKHashEq
   {
      bool operator()( const Clause * a , const Clause * b )const
      {
         extern bool strict_eq( const Clause & a , const Clause & b );
         if( a->size() != b->size() )return false;

         unsigned sz = a->size();
         const Minisat::Lit * x = a->data , * y = b->data;

         for( unsigned i = 0 ; i < sz ; ++i ) 
            if( x[i] != y[i] )
            {
               //assert( strict_eq( *a , *b ) == false );
               return false;
            }
         return true;
      }
   };

   typedef std::tr1::unordered_map< const Clause * , unsigned , CKHashFun , CKHashEq > CKHash;
   vec< vec<unsigned > > _clauses;
   vec< clause_t >       _keaper;
   CKHash                _hash;

   public:
   ~ClauseKeaper()
   {
      for( unsigned i = 0 ; i < _keaper.size() ; ++i ) delete _keaper[i]._ptr;
   }
   /// clause traverse 
   ///
   const Clause * clause( unsigned i , unsigned j )const
   { 
      clause_t k = _keaper[_clauses[i][j]];
      if( k._lvl != i ) return NULL;
      return k._ptr ;
   }
   /// remove the clause not at that level 
   ///
   void remove_redundant_clause()
   {
      for( unsigned i=0;i<_clauses.size();++i)
      {
         unsigned k=0;
         for( unsigned j=0;j<_clauses[i].size();++j)
            if( _keaper[_clauses[i][j]]._lvl == i)
               _clauses[i][k++] = _clauses[i][j];
         _clauses[i].resize(k);
      }
   }
   /// remove clause i , j and push it to i+1
   ///
   void shift_clause( unsigned i , unsigned j )
   {
      unsigned idx = _clauses[i][j];
      _keaper[idx]._lvl +=1 ;
      _clauses[i+1].push( idx );
   }
   void add_clause( const Clause * c , unsigned e )
   {
      clause_t ct = { c , e };      
      unsigned idx =  _keaper.size();
      _hash.insert( std::make_pair( c , idx ) );
      _clauses[e].push( idx );
      _keaper.push( ct );
   }
};

class StateAllocator
{
   friend class IC3; // for IC3info

   vec<uint64_t * > _recycle;
   vec<uint64_t * > _total;
   unsigned         _ptr;
   unsigned         _wstates;

   void addpage()
   {
      uint64_t * tmp = new uint64_t[ _wstates * 256 ];
      _total.push( tmp );
      memset( tmp , 0 , sizeof( uint64_t ) * _wstates * 256 );
      for( int i = 0 ; i < 256 ; ++i )
      {
         _recycle.push( tmp );
         tmp += _wstates;
      }
   }
   public:

   ~StateAllocator(){ for(unsigned i=0;i<_total.size();++i)delete [] _total[i];}
   void init_stalloc( unsigned nstates ){ _wstates = nstates; addpage(); _ptr = 0; } 
   void reset_stalloc(){ _ptr = 0; }
   void resume_stalloc(){ _ptr -=1;}
   State stalloc(){ if( _ptr == _recycle.size() )addpage(); return _recycle[_ptr++]; }

};

#endif
